COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Proof problems for CS206
C00003 ENDMK
C⊗;
Proof problems for CS206

1. NIL*u = u*NIL = u
u*[v*w] = [u*v]*w

2. reverse[u*v] = reverse v * reverse u
reverse reverse u = u
 uses lemmas
rev1[rev1[u,v],w] = rev1[v,u*w]
rev1[u*v,w] = rev1[v,rev1[u,w]]
rev1[u,v] = reverse u * v

3. x ε u*v ≡ x ε u ∨ x ε v

4. correctness of samefringe

5. equivalence of two definitions of flatten

6. sublis and inst are inverses

7. copy is the identity function